pre-init-p2(es;i;ds;init;a;T;P)
== P holds in state init  e@i
== & @i Precondition for a(v)
== & @i P State(ds) (v:T)
== & (x:Id. x  dom(ds)  @i x initially init(x):ds(x)) 

latex

---

clarification:

pre-init-p2(es;i;ds;init;a;T;P)
== pre-init-p(es;i;ds;init;T;P)
== & pre-p(es;i;ds;a;T;P)
== & (x:Id.
== & (fpf-dom(IdDeq; x; ds)  init-p(es; i; fpf-ap(ds; IdDeq; x); x; fpf-ap(init; IdDeq; x))) 

latex

Definitions	P holds in state init  e@i, P & Q, @i Precondition for a(v)P State(ds) (v:T), x:A. B(x), Id, P  Q, b, x  dom(f), @i x initially v:T, f(x), IdDeq
FDL editor aliases	pre-init-p2